%==============================================================================
% Enunciado
%==============================================================================

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "Todos los que ayudan a Juan viven en casa de Manolo. Antonio ayuda a todos
% los que trabajan en su oficina. Todos los amigos de Carlos trabajan en la
% misma oficina que Miguel. Carlos es amigo de Antonio y Miguel trabaja con
% Juan. Por tanto, Antonio vive en casa de Manolo."

%==============================================================================
% Formalización
%==============================================================================

set(binary_res).

formula_list(sos).
% Todos los que ayudan a Juan viven en casa de Manolo.
  all x (ayuda(x,Juan) -> casaManolo(x)).

% Antonio ayuda a todos los que trabajan en su oficina.
  all x (trabajaCon(Antonio,x) -> ayuda(Antonio,x)).

% La relación 'trabajaCon' es simétrica y transitiva.
  all x y (trabajaCon(x,y) -> trabajaCon(y,x)).
  all x y z (trabajaCon(x,y) & trabajaCon(y,z) -> trabajaCon(x,z)).

% Todos los amigos de Carlos trabajan en la misma oficina que Miguel.
  all x (amigos(Carlos,x) -> trabajaCon(Miguel,x)).

% La relación 'amigos' es simétrica.
  all x y (amigos(x,y) -> amigos(y,x)).

% Carlos es amigo de Antonio y Miguel trabaja con Juan.
  amigos(Carlos,Antonio) & trabajaCon(Miguel,Juan).

% Conclusión: Antonio vive en casa de Manolo.
  - casaManolo(Antonio).

end_of_list.

%==============================================================================
